.. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
.. Copyright © 2019 Ariadne Devos

.. index::
   single: slice

Slices: positive-length array ranges
====================================

Slices point to a region in memory, of a certain length.
s² took the concept from Rust [#frustslice]_. Due to
Spectre mitigation issues, slices typically must be
positive in length.

A slice is specified as SliceCap<impl T>(c: T& -> Cap, length:
nat, p: T \*), where `c` indicates the capability.

SliceCap<impl T>(c: T& -> Cap, length: nat, p: T *) :=
  0 <= length <= SIZE_MAX,
  ∀{i | 0 <= i < length} (c . (index a))

.. rubric:: footnotes

XXX Rust reference
